\documentclass[11pt]{article}

\usepackage{multicol}
\usepackage{algorithmic}[5]
\usepackage{algorithm}
\usepackage{amsmath, amsthm, amssymb}
\usepackage{cite}
\usepackage{url}

\setlength{\topmargin}{0in}
\setlength{\headheight}{0cm}
\setlength{\headsep}{0cm}
\setlength{\textheight}{9in}
\setlength{\oddsidemargin}{0cm}
\setlength{\evensidemargin}{0cm}
\setlength{\textwidth}{6.5in}

\renewcommand{\algorithmiccomment}[1]{// #1}
\renewcommand{\algorithmicensure}{\textbf{define}}

\begin{document}

\title{Design and Implementation of a\\
Hybrid-Typed Programming Language:\\
Project Proposal}

\author{Michael M. Vitousek\\
Willamette University\\
\texttt{mmvitousek@gmail.com}}
\date{May 5, 2010}
\maketitle


\begin{abstract}
Numerous approaches to the problem of determining the correctness of computer programs have been proposed and implemented, such as dynamic and static type checking. Static typing enables earlier error checking and more efficient execution in many programs, while dynamic type systems allow for full expressiveness and greater flexibility. This paper proposes the creation of a type system, referred to as hybrid typing, that integrates some of the advantages of both typechecking paradigms, and the development of a programming language, Gnarly, that utilizes hybrid typing and demonstrates its benefits and abilities. \end{abstract}

	\section{Introduction}
	Programming languages are classified in a number of ways and one important way is how they treat the types of a program. Types classify the information within a program and arise from the need for a system to reject nonsensical operations. They are handled by a number of different techniques in different systems, but most current type systems may be broadly classified into two categories. Static type systems analyze type data in a program at compile time and reject the program if any type errors (situations where the provided type does not match the expected type of an operation or identifier) are detected. Otherwise, if no type errors are found, static type systems allow the program to assume at runtime that all type information in the program is accurate and no further checking is required\cite{pierce}. Dynamic type systems operate on a very different principle. They reject bad programs at runtime rather than compile time, by tagging program data with type information and using that information to detect type errors. Static systems give a measure of security to the programmer and allow  abstract analysis of a program's behavior, but because  not all possible programs are expressible in a static language, static type systems reject some programs that are in fact computable\cite{pierce}. Dynamic languages allow for more flexibility because of their lack of conservative compile time analysis, but this same flexibility allows for type errors that are not caught until runtime.  

	This project, therefore, aims to develop a type system, to be referred to as ``hybrid typing,'' that allows for the expressiveness of dynamic type systems but preserves some of the safeties of static typing. This project also will entail the development of a programming language that implements this type system. By melding static and dynamic type systems, this language will still have the ability to determine correctness at compile time for all sections of code that are not explicitly or implicitly dynamic, but will give the programmer the option to perform operations and write programs that a purely static system would reject.  

	\section{Project Proposal}
	Hybrid typing is intended to be a type system for a simple, but highly expressive and not trivially small, programming language that will allow it to utilize features from both the static and dynamic families of type systems. This language, referred to as Gnarly,\footnote{The name ``Gnarly'' has no meaning specific to the language but is intended to be memorable, upbeat, and informal, and is a reference to the influence of the Groovy programming language\cite{barclay}, another integrative language which melds functional semantics with a Java-like syntax.} will be in the functional programming paradigm and be a superset of the lambda calculus, and hybrid typing will allow for the language to be written either purely dynamically, purely statically, or as a mix, thereby achieving the full spectrum of possible uses and abilities.
	\subsection{Motivation}
	The division of programming languages into those using static type systems, and those that are dynamic, contributes to the specialization of programming languages for different uses. Static type systems, since they can guarantee a program is free of type errors before the program is ever executed and may make the meaning of a program more apparent to inspection, are naturally popular in contexts where reliability and consistency is extremely important\cite{pierce}. Such cases include most large, commercial applications --- it is naturally important for any software company to minimize bugs before placing their products on the market. On the other hand, dynamic systems are popular when flexibility is important such as in Web applications, explaining the use of dynamic typing in Web oriented languages such as PHP and JavaScript. Furthermore, the ability of dynamically typed languages to express any possible program contributes to the popularity of those languages in academics and research, as illustrated by Scheme, Haskell, and on a more basic level, the untyped lambda calculus.

	Although such specialization causes certain languages to excel in certain applications, it may also be limiting, as it denies languages access to some features that may in some situations be helpful, even if not crucial. For example, it may be useful to prototype large programs in a dynamic style while the exact demands and abilities of the program are still undefined, before transferring it to a static form once its design specifications are no longer nebulous. Integrating static and dynamic type checking into the same system, such as by allowing portions of code to be unchecked at compile time and only checked at runtime, while continuing to statically check the remainder of the program, may meet this challenge.
	\subsection{Overview}
	The final result of this project will be a fully functional interpreter or compiler for the Gnarly language, basic documentation for its use, a specification for Gnarly, and a basic overview of how to write programs in Gnarly, including examples of basic algorithms such as sorts or the Sieve of Eratosthenes. The Gnarly programming language itself will have a syntax similar to other functional programming languages, though which in particular is presently undecided. Possibilities include the parenthetical syntax of Scheme or the more familiar (to most programmers), imperative-like syntax of Haskell or ML. 

	The primary goal of the hybrid type system of Gnarly is to achieve in particular two distinct advantages from other type systems, one from static typing and one from dynamic typing:
\begin{enumerate}
\item It should allow the expression of all possible programs, even those which may contain type errors, when so desired by the programmer, and in such cases detect and report type errors at runtime.
\item It should, when \emph{not} otherwise specified,\footnote{Given a sufficiently broad definition of ``specified.''} catch all type errors at compile time.
\end{enumerate}
If, in the course of the project, it is discovered that this behavior is impossible, or impossible without a dramatically different approach to the system, the system will be developed to come as close to these goals as possible while still remaining useful as a type system in a ``real'' language, with the cases where such behavior is not possible being clearly defined and specified. The system will integrate other advantages and disadvantages from other type systems if possible, but these two are the central goals of the development of hybrid typing.

	Gnarly's typechecker will likely achieve this objective through using both static and dynamic typechecking along with the addition of a ``\textsf{dynamic}'' type label. This \textsf{dynamic} may be used in the same ways as the usual \textsf{integer}, \textsf{string}, \textsf{boolean}, etc type labels used in most explicit static type systems --- it may be applied to identifiers such as variables or method names, and means that the value of that identifier (in the case of a method, the return value) is unspecified at compile time. A substantial concern to the design of this system is how dynamic and static portions of the same program interact during static interpretation; for example, consider a situation in which a method expects a statically typed \textsf{integer} as an argument, but is instead provided with an identifier of type \textsf{dynamic}. One approach may be to have the static typechecker always consider such an operation to be well-typed, and another may be to require further programmer specification such as casting, and a third may be simply rejecting such an operation.

	Beyond its type system, Gnarly should be a small-to-medium sized functional language, capable of easily expressing most standard sorting algorithms but without supporting object-oriented constructs or advanced features like first-class continuations. It will, at least initially, be evaluated by interpretation, either directly or by conversion to an intermediate language using tools like lex and yacc. Compilation to machine code or Java bytecode is outside of the primary scope of this project, but if all key milestones are achieved with substantial time to spare, such an addition to the project may be considered. An eager call-by-value strategy will be used in the first pass at the evaluation procedures, but call-by-name (i.e.\ lazy) evaluation may be eventually implemented instead, or as an alternative version of the language.
	\subsection{Related Work}
	This project is not the first attempt at integrating dynamic and static typing features. Some previous approaches include the system of Abadi et al.\cite{abadi91}, Satish Thatte's quasi-static typing\cite{thatte90}, and Cartwright and Fagan's soft typing\cite{cartwright91} from the early 1990s, as well as Cormac Flanagan's hybrid typing (unrelated in specifics to this project)\cite{flanagan06} and Siek and Taha's gradual typing\cite{siek06} from 2006. These systems are designed to solve the same problem approached in this project, and they do so in broadly similar ways. Mart\'{i}n  Abadi's group uses an explicit \textsf{Dynamic} construct, and Thatte's $\Omega$-type fulfills the same purpose as my \textsf{dynamic} --- explicitly forcing a section of the program to be checked dynamically. Semantically, however, these languages negotiate the space between static and dynamic checking in a different way, mostly by inserting run-time checks where necessary, than this project's (intended) technique of having mirrored static and dynamic checks, and while the \textsf{dynamic} type used in this project is intended to serve as a ``pseudo-type'' that acts as a flag to the type system, the \textsf{Dynamic} of Abadi et al.\ and Thatte's $\Omega$ are closer to the \textsf{Object} class in Java, for example. Furthermore, these papers are all strictly specifications for type systems, applied to variants of the lambda calculus rather than to a more generally useful language. This project intends to develop both system and language, creating something of immediate practical, as well as theoretical, interest.
	\subsection{Major Milestones}
	There are a number of subgoals involved in this project. At first approximation, there are two major branches to the project: design and implementation of an interpreter or compiler for the language, and development of the type system. Milestones for the language implementation seem clear: a specification and interpreter for basic arithmetic expressions will be a good starting point for creating grammars, learning how to develop language semantics, and working out parsing and interpretation issues. This language will then be grown to include more structures and operations --- exactly which ones will be decided during development of the language and typing semantics, but they will all be standard for functional languages. This portion of the project is very well-studied, and references and sources will be plentiful.
	
	On the type system side, it may make sense to start with a straightforward dynamic type system that could be integrated with the nascent language described above, and after this, a straightforward static typechecker. After both are complete, experimenting with and altering the type judgment rules for both systems to accommodate the \textsf{dynamic} construct would be the next logical step. The limits, both absolute and in terms of feasibility, of what is possible here are unclear, so part of this phase of the project would be determining those limits, and if necessary, moving the goalposts for the completed type system to fit into them. This portion of the project is less well-known, with most previous approaches being experimental.
	
	Given these goals, a minimum completion point for the project may be the development and implementation of a small but complete, dynamically typed programming language. This would be putting aside the goal of integrating static features in favor of the work of implementing a programming language and ensuring that it is possible and practical to actually write code in. Such a result would not be especially \emph{interesting}, as there are numerous such languages already, but would at least demonstrate mastery of the central tenets of programming language design and implementation.
	\section{Timeline}
	To decrease workload during Fall Semester 2010, I aim to have most or all of the implementation portion of this project completed during the Summer months, leaving writing my paper, documentation, and other important elements of the project for the Fall. The below schedule is of course highly subject to change, in the case that I find a section is more difficult to complete than I imagined, I am unable to work for a period of time (e.g.\ due to illness), or I simply need to focus on work for classes. The dates below are the Mondays (in the Summer) or Tuesdays (in the Fall, because thesis class is held on Tuesdays) of the week in which I will work on the objective given --- they are not when the objective should be finished by, but rather the beginning of the period in which the objective will be worked on.
	\subsection{Summer 2010}
\begin{tabular}{rlp{4.7in}}
May & 24 & Develop a grammar for a language of arithmetic expressions, begin implementation of an interpreter for it. \\
May & 31 & Finish interpreter. Grow the grammar and semantics of the language to include at least one more type beyond natural numbers.\\
June & 7 & Work on a dynamic type checker for the language. \\
June & 14 & At University of Oregon Programming Language Summer School most of this week, little work will be done.\\
June & 21 & At University of Oregon Programming Language Summer School most of this week, little work will be done. \\
June & 28 & Add control structures to language, implement in type checker\\
July & 5 & Add function abstraction and application to language, implement in type checker.\\
July & 12 & Work on a static type checker for the language.\\
July & 19 & Keep working on static typing. \\
July & 26 & Going to Maine for a wedding this week. Don't know how much work I will be able to do, but I will catch up on any loose ends at the very least.\\
August & 2 & Experiment with adding the \textsf{dynamic} label to the type system --- look at ramifications on grammar, semantics, etc.\\
August & 9 & Work on implementing \textsf{dynamic} into the static type checker.\\
August & 16 & Complete initial pass at \textsf{dynamic}. \\
August & 23 & Work on better integrating the type systems --- e.g., see if it's possible to formally describe cases when the dynamic type checker does not need to operate for efficiency.\\
August & 30 & Last day of summer, not working. \\
\end{tabular}
	\subsection{Fall Semester 2010}
	\begin{tabular}{rlp{4.5in}}
August & 31 & Catch up period. Try to complete anything left over from summer.\\
September & 7 & Catch up period. Try to complete anything left over from summer.\\
September & 14 & Add any additional language features not yet implemented. Finalize language design. \\
September & 21 & Investigate type safety of language. \\
September & 28 & Investigate type safety of language. \\
October & 5 & Work on first draft of paper. \\
October & 12 & Work on and finish first draft of paper. This target date subject to change based on expectations of the thesis class.\\
October & 19 & Work on any remaining implementation concerns. \\
October & 26 & Work on any remaining implementation concerns. Ideally, finalize language and type system implementation. \\
November & 2 & Create the final written specification of language. \\
November & 9 & Work on programmer's guide, write code in language. \\
November & 16 & Finish programmer's guide and work on paper. \\
November & 23 & Write guide for use of interpreter or compiler, work on paper.\\
November & 30 & Work on paper and presentation. \\
December & 7 & Work on paper and presentation. \\
December & 14 & Present and submit project.\\
\end{tabular}
	\section{Conclusions}
	Hybrid typing and Gnarly are intended to be potential solutions to the problem of flexibility versus correctness. A language correctly written in Gnarly may be statically typed where desired and dynamically typed when needed, allowing programmers to have the expressiveness of languages like Scheme, the flexibility of languages like ML, and the early detection of errors of languages like Java. For programmers familiar with dynamic languages and also accustomed to writing programs in a simply typed style, little additional overhead will be required from programmers beyond using the \textsf{dynamic} pseudo-type when flexibility is needed from the language. Although integrating the paradigms of static and dynamic typing has been explored in some detail in the past, in many cases such implementations were restricted to the lambda calculus. This project aims to both develop such a system, and to create a programming language with enough high level constructs and operations to be easily coded in by programmers of moderate experience.
\bibliographystyle{plain}
\bibliography{latex/SelectedBibliography}
\end{document}
